elt:=#:atom.
rel:=(x,y:elt)bool:(x,y:elt)atom.

rpred(r:rel;x:elt):=r(x,x):bool.
reflexive(r:rel):=for_all(elt,rpred(r)):bool.
use_reflexivity(x:elt;r:rel;p:proof(reflexive(r)))
 :=specialize(elt,rpred(r),x,p):proof(r(x,x)).

spred2(r:rel;x,y:elt):=implies(r(x,y),r(y,x)):bool.
spred1(r:rel;x:elt):=for_all(elt,spred2(r,x)):bool.
symmetric(r:rel):=for_all(elt,spred1(r)):bool.
use_symmetry(x,y:elt;r:rel;p:proof(symmetric(r));q:proof(r(x,y)))
 :=modus_ponens(r(x,y),r(y,x),
  specialize(elt,spred2(r,x),y,specialize(elt,spred1(r),x,p)),q):proof(r(y,x)).

tpred3(r:rel;x,y,z:elt):=implies(and(r(x,y),r(y,z)),r(x,z)):bool.
tpred2(r:rel;x,y:elt):=for_all(elt,tpred3(r,x,y)):bool.
tpred1(r:rel;x:elt):=for_all(elt,tpred2(r,x)):bool.
transitive(r:rel):=for_all(elt,tpred1(r)):bool.
use_transitivity(x,y,z:elt;r:rel;p:proof(transitive(r));
 p1:proof(r(x,y)); p2:proof(r(y,z))):=
 modus_ponens(and(r(x,y),r(y,z)),r(x,z),
  specialize(elt,tpred3(r,x,y),z,specialize(elt,tpred2(r,x),y,
    specialize(elt,tpred1(r),x,p))),
  conjunction(r(x,y),r(y,z),p1,p2)):proof(r(x,z)).

rs_rel(r:rel):=and(reflexive(r),symmetric(r)):bool.
equiv_rel(r:rel):=and(rs_rel(r),transitive(r)):bool.
refl_equiv(r:rel;p:proof(equiv_rel(r))):=
 first_conjunct(reflexive(r),symmetric(r),
  first_conjunct(rs_rel(r),transitive(r),p)):proof(reflexive(r)).
symm_equiv(r:rel;p:proof(equiv_rel(r))):=
 second_conjunct(reflexive(r),symmetric(r),
  first_conjunct(rs_rel(r),transitive(r),p)):proof(symmetric(r)).
trans_equiv(r:rel;p:proof(equiv_rel(r))):=
 second_conjunct(rs_rel(r),transitive(r),p):proof(transitive(r)).

set:=(x:elt)bool:(x:elt)atom.
in(x:elt;s:set):=proof(s(x)):atom.

incl_pred(s,t:set;x:elt):=implies(s(x),t(x)):bool.
set_incl(s,t:set):=for_all(elt,incl_pred(s,t)):bool.
is_incl(s,t:set):=proof(set_incl(s,t)):atom.
set_move(s,t:set;p:is_incl(s,t);x:elt;q:in(x,s)):=
 modus_ponens(s(x),t(x),specialize(elt,incl_pred(s,t),x,p),q):in(x,t).

set_incl_refl(s:set):=
 generalize(elt,incl_pred(s,s),(x:elt)imp_refl(s(x))):is_incl(s,s).

step1(s,t,u:set;p:is_incl(s,t);q:is_incl(t,u);x:elt):=
 implication(s(x),u(x),(r:in(x,s))set_move(t,u,q,x,set_move(s,t,p,x,r))):
 proof(incl_pred(s,u,x)).
set_incl_trans(s,t,u:set;p:is_incl(s,t);q:is_incl(t,u)):=
 generalize(elt,incl_pred(s,u),step1(s,t,u,p,q)):is_incl(s,u).

set_eq(s,t:set):=and(set_incl(s,t),set_incl(t,s)):bool.
is_eq(s,t:set):=proof(set_eq(s,t)):atom.

set_eq_refl(s:set):=
 conjunction(set_incl(s,s),set_incl(s,s),set_incl_refl(s),set_incl_refl(s)):
 is_eq(s,s).
set_eq_symm(s,t:set;p:is_eq(s,t)):=
 and_symm(set_incl(s,t),set_incl(t,s),p):is_eq(t,s).

step1(s,t,u:set;p:is_eq(s,t);q:is_eq(t,u)):=
 set_incl_trans(s,t,u,first_conjunct(set_incl(s,t),set_incl(t,s),p),
  first_conjunct(set_incl(t,u),set_incl(u,t),q)):is_incl(s,u).
step2(s,t,u:set;p:is_eq(s,t);q:is_eq(t,u)):=
 step1(u,t,s,set_eq_symm(t,u,q),set_eq_symm(s,t,p)):is_incl(u,s).
set_eq_trans(s,t,u:set;p:is_eq(s,t);q:is_eq(t,u)):=
 conjunction(set_incl(s,u),set_incl(u,s),step1(s,t,u,p,q),step2(s,t,u,p,q)):is_eq(s,u).

E:=#:rel.
assumption:=#:proof(equiv_rel(E)).
I(x,y:elt):=proof(E(x,y)):atom.
E_refl(x:elt):=use_reflexivity(x,E,refl_equiv(E,assumption)):I(x,x).
E_symm(x,y:elt;p:I(x,y)):=
 use_symmetry(x,y,E,symm_equiv(E,assumption),p):I(y,x).
E_trans(x,y,z:elt;p:I(x,y);q:I(y,z)):=
 use_transitivity(x,y,z,E,trans_equiv(E,assumption),p,q):I(x,z).

proposition0(x:elt):=E_refl(x):in(x,E(x)).

step1(x,y,z:elt;p:I(x,y);q:I(x,z)):=E_trans(y,x,z,E_symm(x,y,p),q):I(y,z).
step2(x,y:elt;p:I(x,y);z:elt):=implication(E(x,z),E(y,z),step1(x,y,z,p)):
 proof(implies(E(x,z),E(y,z))).
lemma1(x,y:elt;p:I(x,y)):=generalize(elt,incl_pred(E(x),E(y)),step2(x,y,p)):
 is_incl(E(x),E(y)).
proposition1(x,y:elt;p:I(x,y)):=
 conjunction(set_incl(E(x),E(y)),set_incl(E(y),E(x)),
  lemma1(x,y,p),lemma1(y,x,E_symm(x,y,p))):
 is_eq(E(x),E(y)).

step1(x,y:elt;p:is_eq(E(x),E(y))):=
 first_conjunct(set_incl(E(x),E(y)),set_incl(E(y),E(x)),p):is_incl(E(x),E(y)).
step2(x,y:elt;p:is_eq(E(x),E(y))):=
 specialize(elt,incl_pred(E(x),E(y)),x,step1(x,y,p)):
 proof(implies(E(x,x),E(y,x))).
proposition2(x,y:elt;p:is_eq(E(x),E(y))):=
 E_symm(y,x,modus_ponens(E(x,x),E(y,x),step2(x,y,p),E_refl(x))):I(x,y).

Eclass(s:set;x:elt):=set_eq(s,E(x)):bool.
is_Eclass(s:set):=proof(exists(elt,Eclass(s))):atom.

Erep(s:set;p:is_Eclass(s)):=choose(elt,Eclass(s),p):elt.
IErep(s:set;p:is_Eclass(s)):=thus(elt,Eclass(s),p):is_eq(s,E(Erep(s,p))).

step1(s:set;p:is_Eclass(s)):=
 first_conjunct(set_incl(s,E(Erep(s,p))),set_incl(E(Erep(s,p)),s),IErep(s,p)):
 is_incl(s,E(Erep(s,p))).
proposition3(s:set;p:is_Eclass(s);x:elt;q:in(x,s)):=
 set_move(s,E(Erep(s,p)),step1(s,p),x,q):I(Erep(s,p),x).

meets(s,t:set):=exists(elt,(x:elt)and(s(x),t(x))):bool.
disjoint_or_equal(s,t:set):=implies(meets(s,t),set_eq(s,t)):bool.

common_elt(s,t:set;p:proof(meets(s,t))):=
 choose(elt,(x:elt)and(s(x),t(x)),p):elt.
common_first(s,t:set;p:proof(meets(s,t))):=
 first_conjunct(s(common_elt(s,t,p)),
  t(common_elt(s,t,p)),thus(elt,(x:elt)and(s(x),t(x)),p)):in(common_elt(s,t,p),s).
common_second(s,t:set;p:proof(meets(s,t))):=
 second_conjunct(s(common_elt(s,t,p)),
  t(common_elt(s,t,p)),thus(elt,(x:elt)and(s(x),t(x)),p)):in(common_elt(s,t,p),t).

step1(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 proposition3(s,p,common_elt(s,t,r),common_first(s,t,r)):
 I(Erep(s,p),common_elt(s,t,r)).
step2(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 proposition3(t,q,common_elt(s,t,r),common_second(s,t,r)):
 I(Erep(t,q),common_elt(s,t,r)).
step3(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 E_trans(Erep(s,p),common_elt(s,t,r),Erep(t,q),step1(s,t,p,q,r),
  E_symm(Erep(t,q),common_elt(s,t,r),step2(s,t,p,q,r))):
 I(Erep(s,p),Erep(t,q)).
step4(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 proposition1(Erep(s,p),Erep(t,q),step3(s,t,p,q,r)):
 is_eq(E(Erep(s,p)),E(Erep(t,q))).
step5(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 IErep(s,p):is_eq(s,E(Erep(s,p))).
step6(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 IErep(t,q):is_eq(t,E(Erep(t,q))).
step7(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 set_eq_trans(s,E(Erep(s,p)),E(Erep(t,q)),step5(s,t,p,q,r),step4(s,t,p,q,r)):
 is_eq(s,E(Erep(t,q))).
step8(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 set_eq_trans(s,E(Erep(t,q)),t,step7(s,t,p,q,r),
  set_eq_symm(t,E(Erep(t,q)),step6(s,t,p,q,r))):
 is_eq(s,t).
proposition4(s,t:set;p:is_Eclass(s);q:is_Eclass(t)):=
 implication(meets(s,t),set_eq(s,t),step8(s,t,p,q)):
 proof(disjoint_or_equal(s,t)).